T:Type, P:((T List)Prop), f:(T). safety(T;L.P(L))  safety(T;L.P(filter(f;L))) 

latex

Definitions	t  T, Prop, , P  Q, x:A. B(x), l1  l2, filter(P;l), safety(A;tr.P(tr))
Lemmas	filter iseg, filter wf, iseg wf, bool wf